Proj: Natural number gameを解く

Natural number game

Lean 4版

Natural Number Game

Lean 4 基礎

rfl

Goalが左辺=右辺なら証明完了

rw [one_eq_succ_zero]

1ならsucc 0になる

rw [← one_eq_succ_zero]で定理？を逆向きに適用する

succ 0なら1になる

rw(Lean 4)

ログ

Tutorial World

First unravel the 1.

Natural Number Game in Lean 4 - Episode 0 Defining Natural Numbers - YouTube

2024-03-02

Tutorial worldまでクリアできた

rw [one_eq_succ_zero] でn+1の1をsucc 0にできる

rw [add_succ]で n + succ 0 → succ (n + 0)にできる

rw [add_zero]でsucc (n + 0)をsucc nにできる

右上の</>をクリックするとエディターモードになる

inductionはinduction n with d hd のように書く

induction: 帰納法 - Lean4 タクティク逆引きリスト

induction

2024-05-12

Level 2 / 5 : succ_add

code:memo

induction b with h hd

rw add_zero

rw ← add_succ

rw ← one_eq_succ_zero

rw succ_eq_add_one

rfl

rw add_succ, add_succ

rw hd

rfl

assumption(仮定)のhdで、ゴールをrwできることがわかれば解けるようになる

2024-05-15

Multiplication World完了、Implication World完了

repeatはrepeat rw [zero_add] at hのように使う

intro hで仮定を作る？

exact hで仮定とゴールを比較する

apply h2 at h1なら仮定h2を仮定h1に適用する

code:memo

h1: x = 37

h2: x = 37 → y = 42

↓ (apply h2 at h1)

h2: x = 37 → y = 42

h1: y = 42

apply succ_inj at hなら仮定hのsuccを除去する

succ(a) = succ(b)→a = b

code:memo

h: succ (succ 0) = succ (succ (succ 0))

↓ apply succ_inj at h

h: succ 0 = succ (succ 0)

apply succ_injならゴールに適用する

メモ

exact: 証明を直接構成 - Lean by Example

apply(Lean)

2024-05-19

2024-05-19#664a1c15e587fd0000b9c331

2024-06-03

World: Algorithm World Level 6 / 9 : is_zero

code:memo.lean

theorem succ_ne_zero (a : ℕ) : succ a ≠ 0 := by

intro h

-- h: succ a = 0, Goal: is_zero (succ a)

rw ← is_zero_succ a

trivial

Goal: is_zero (succ a)のときにtrivialにすると解決される

trivial(Lean)

仮定hが矛盾

World: Algorithm World Level 8 / 9 : decide

型クラスのインスタンスが定義されているのでdecideでいい感じに証明してくれるらしい

code:instDecidableEq.lean

instance instDecidableEq : DecidableEq ℕ

| 0, 0 => isTrue <| by

show 0 = 0

rfl

| succ m, 0 => isFalse <| by

show succ m ≠ 0

exact succ_ne_zero m

| 0, succ n => isFalse <| by

show 0 ≠ succ n

exact zero_ne_succ n

| succ m, succ n =>

match instDecidableEq m n with

| isTrue (h : m = n) => isTrue <| by

show succ m = succ n

rw h

rfl

| isFalse (h : m ≠ n) => isFalse <| by

show succ m ≠ succ n

exact succ_ne_succ m n h

decide、Decidableについて

型クラス - Theorem Proving in Lean 4 日本語訳

decide(Lean 4)

2024-08-xx

comtraposeタクティクを使うと良い場合がある

contrapose(Lean)

2024-09-21

le_transはわからなかったので答えを見た...

https://github.com/adyavanapalli/natural-number-game-solutions/blob/master/inequality-world/5

use(Lean 4)

Level 4 / 11 : x ≤ y and y ≤ z implies x ≤ z

code:memo

theorem le_trans (x y z : ℕ) (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by

cases hxy with a ha

cases hyz with b hb

rw hb

rw ha

use (a + b)

rw add_assoc x a b

rfl

2024-10-12

≤ World Level 5 / 11 : x ≤ 0 → x = 0

code:lean

theorem le_zero (x : ℕ) (hx : x ≤ 0) : x = 0 := by

cases x

rfl

cases hx

symm at h

contrapose h

rw succ_add

apply succ_ne_zero

なぜ証明できているか全然わからない。どうしてcases hxを使用するとassumptionsがsucc a ≦ 0からh: 0 = succ a + wに変化するのか全然わからない

code:memo

Objects:

a: ℕ

Assumptions:

hx: succ a ≤ 0

Goal:

succ a = 0

↓

Current Goal

Objects:

aw: ℕ

Assumptions:

h: 0 = succ a + w

Goal:

succ a = 0

2024-10-14

Level 6 / 11 : x ≤ y and y ≤ x implies x = y

何をしたらよいかわからなくなった

code:memo

-- ≤の場合の反対称律

-- まだ解けていない

theorem le_antisymm (x y : ℕ) (hxy : x ≤ y) (hyx : y ≤ x) : x = y := by

cases x with d1 hd1

cases y with d2 hd2

rfl

cases hyx

rw succ_add at h

rw h

symm

contrapose h

apply zero_ne_succ

cases hxy with d3 hd3

rw succ_add at hd3

cases hyx with d4 hd4

rw hd3 at hd4

rw succ_add at hd4

symm

rw hd3

rw hd4

contrapose! hd4

apply succ_ne_succ

-- intro h

-- symm at h

-- apply h at hd4

反対称律

#My_Project